\begin{frame}
\frametitle{Zusammenfassung}
\begin{itemize}
\item Beim \emph{Model-Checking} wird für ein gegebenes Modell überprüft, ob eine Spezifikation erfüllt ist.
\item Das \emph{Model-Checking} basiert auf temporalen Logiken, z.B. CTL.
\item \emph{Model-Checker} verifizieren automatisch ein gegebenes Modell.
\begin{itemize}
\item Und liefern gegebenenfalls ein konkretes Gegenbeispiel
\end{itemize}
\item Der Zustandsraum muss endlich sein.
\end{itemize}
\end{frame}